\begin{tabbing}
R{-}names($A$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $A$ of \+
\\[0ex]Rnone =$>$ []
\\[0ex]Rplus(${\it left}$,${\it right}$)=$>$${\it rec}_{1}$,${\it rec}_{2}$.${\it rec}_{1}$ @ ${\it rec}_{2}$
\\[0ex]Rinit(${\it loc}$,$T$,$x$,$v$)=$>$ [(inr $<$${\it loc}$, $x$$>$ ) / []]
\\[0ex]Rframe(${\it loc}$,$T$,$x$,$L$)=$>$ [(inr $<$${\it loc}$, $x$$>$ ) / []]
\\[0ex]Rsframe(${\it lnk}$,${\it tag}$,$L$)=$>$ [(inl locknd(destination(${\it lnk}$);rcv(${\it lnk}$,${\it tag}$)) ) / []]
\\[0ex]Reffect(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$)=$>$ [\=(inl locknd(${\it loc}$;${\it knd}$) ); \+
\\[0ex]
\\[0ex](inr $<$${\it loc}$, $x$$>$ ) / map($\lambda$$x$.inr $<$${\it loc}$, $x$$>$ ;fpf{-}domain(${\it ds}$))]
\-\\[0ex]Rsends(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$)=$>$ [\=(inl locknd(source($l$);${\it knd}$) ) / \+
\\[0ex](map($\lambda$$x$.inr $<$source($l$), $x$$>$ ;fpf{-}domain(${\it ds}$))
\\[0ex]@ map\=($\lambda$${\it tg}$.inl locknd(destination($l$);rcv($l$,${\it tg}$)) \+
\\[0ex];\=remove{-}repeats(IdDeq;fpf{-}domain(${\it dt}$)\+
\\[0ex]@ map($\lambda$$x$.$x$.1;$g$))))]
\-\-\-\\[0ex]Rpre(${\it loc}$,${\it ds}$,$a$,$T$,$P$)=$>$ [\=(inl locknd(${\it loc}$;locl($a$)) ) / \+
\\[0ex]map($\lambda$$x$.inr $<$${\it loc}$, $x$$>$ ;fpf{-}domain(${\it ds}$))]
\-\\[0ex]Rkframe(${\it loc}$,$k$,$L$)=$>$ [(inl locknd(${\it loc}$;$k$) ) / []]
\\[0ex]Rksframe(${\it loc}$,$k$,$L$)=$>$ [(inl locknd(${\it loc}$;$k$) ) / []]
\\[0ex]Rrframe(${\it loc}$,$x$,$L$)=$>$ [(inr $<$${\it loc}$, $x$$>$ ) / []]
\-
\end{tabbing}